#ifndef __PDTSCTRAVERSAL_H_
#define __PDTSCTRAVERSAL_H_

#include <iostream>
#include <PDTTraversalIFC.h>
#include <PDTAbcObj.h>
#include <map>
#include <PDTPCTraversal.h>
#include <PDTGraphClone.h>
#include <PDTSCUtil.h>

extern PDTCodeGraph * 
mini_main(const string & file);

class PDTCodeGraph;
class PDTAdd;
class PDTNumVar;
class PDTIfElse;
class PDTStatment;
class PDTListOfStatements;
class PDTWhile;
class PDTAnd;
class PDTLessThan;
class PDTGreaterThan;
class PDTGreaterThanEqual;
class PDTEqualNum;
class PDTNotEqualNum;
class PDTPreCondition;
class PDTPostCondition;
class PDTImplies;
class PDTNot;
class PDTPiAssign;

typedef class PDTPCHolder PCValues_t;

class PDTSCTraversal: public Traversal {
    public:
        PDTCodeGraph cg; 
        PDTGraphCloneTraversal gClone;
        unsigned int nodeId;
        //TODO: Check if it should be PDTAbcObj** to hold pointers
        PDTAbcObj ** id2Obj;
        Id2Pc_t id2pc;
        PDTNumAbcObj * pc; 
        unsigned int size;
        unsigned int bound;
        unsigned int pc_count;
        Abc_Ntk_t * pAig;
        PDTNumAbcObj ** pcObjs;
        PDTNumAbcObj * pcPlusOne;
        PDTBoolAbcObj * PDTAbcZero;
        PDTBoolAbcObj * PDTAbcOne;
        PDTPCTraversal pcTraverse;
        unsigned int arrayBound;
        bool abc_debug;

        PDTSCTraversal(PDTCodeGraph & CG, unsigned int aNodeId, unsigned int aBound, bool aAbc_debug, unsigned int arrBound = 0); 

        ~PDTSCTraversal(); 

        ////////// Needed methods //////////
        virtual Traversal::RetType post(PDTAdd & d);
        virtual Traversal::RetType post(PDTNumVar & d);
        virtual Traversal::RetType post(PDTAssign & d);
        virtual Traversal::RetType post(PDTPiAssign & d);
        virtual Traversal::RetType post(PDTNumConstInt & d);
        virtual Traversal::RetType post(PDTBoolConst & d);
        virtual Traversal::RetType post(PDTBoolVar & d);
        virtual Traversal::RetType post(PDTIfElse & d);
        virtual Traversal::RetType post(PDTWhile & d);
        virtual Traversal::RetType post(PDTAnd & d);
        virtual Traversal::RetType post(PDTOr & d);
        virtual Traversal::RetType post(PDTSequenceVar & d);
        virtual Traversal::RetType post(PDTSequenceAccessNum & d);
        virtual Traversal::RetType post(PDTSequenceAccessBool & d);
        virtual Traversal::RetType post(PDTLessThan & d);
        virtual Traversal::RetType post(PDTGreaterThan & d);
        virtual Traversal::RetType post(PDTGreaterThanEqual & d);
        virtual Traversal::RetType post(PDTEqualNum & d);
        virtual Traversal::RetType post(PDTListOfStatements & d);
        virtual Traversal::RetType post(PDTLessThanEqual & d);
        virtual Traversal::RetType post(PDTAssert & d);
        virtual Traversal::RetType post(PDTPreCondition & d);
        virtual Traversal::RetType post(PDTPostCondition & d);
        virtual Traversal::RetType post(PDTImplies & d);
        virtual Traversal::RetType post(PDTNot & d);
        virtual Traversal::RetType post(PDTNotEqualNum & d);


        /**
         * @brief Traverse Code Graph Variables
         */
        void traverseVariables();

        /**
         * @brief Assign PCValues 
         * @return Updates the id2pc map
         */
        void updatePC();

        /**
         * @brief Given an input vector of bits to choose from according to a 
         * specified vector control input.
         * @return returns the selected bit from the input vector
         * Originally written by Mario Achkar
         */
        PDTBoolAbcObj * buildMux(
                PDTNumAbcObj & inps,   //!< The input vector of bits
                PDTNumAbcObj & control //!< The input control vector
                );

        /**
         * @brief Given a set of input vectors of bits, the mux returns the 
         * selected set according to the given control input vector. 
         * Each vector at i represents the ith bit for each of the input vectors. 
         * @return returns the selected bit vector
         * Originally written by Mario Achkar
         * TODO: Optimization can be made here
         */
        PDTNumAbcObj * 
        buildMuxVec(vector < PDTNumAbcObj * > & inps, //!< Input 2D vector of bits
                PDTNumAbcObj & control //!< Input control vector
                );

        /**
         * @brief build a one bit mux with vector inputs
         * @return PDTNumAbcObj * with the required return value
         */
        PDTNumAbcObj * 
        buildOneBitMux(PDTNumAbcObj & in0, //!< The input vector to return at 0
                PDTNumAbcObj & in1, //!< The input vector to be return at 1
                PDTBoolAbcObj & cntrl //!< The input control
                );

        /**
         * @brief This method creates latches as well as inputs and ouputs 
         * for a given variable.
         * @return returns a vector of objects representing the latches' outputs
         * TODO: check whether should build mux here
         */
        PDTNumAbcObj * 
        buildVariable(PDTVar & var //!< the numvar to build
                );

        PDTNumAbcObj *
        buildVariable(PDTVar & var, //!< the numvar to build
                unsigned int specialBound //!< the special bound it has
                );

        PDTNumAbcObj *
        buildVariable();

        /**
         * @brief Create a latch for a one bit variable
         * @return PDTBoolAbcObj * 
         */
        PDTBoolAbcObj *
        buildOneBitVar(PDTVar & var //!< the boolean var to build
                );

        /**
         * @brief This method sets up the representation of the program counter
         * @return returns a vector pointing to the latches as well as 
         * the input and output vectors
         */
        PDTNumAbcObj *
        buildPC(unsigned int length //!< The length of the pc
               );

        /**
         * @brief Builds an n bit adder to be used as an ALU for addition
         * @return returns a vector of bits as sum and an overflow flag
         * Originally written by Mario Achkar
         */
        PDTNumAbcObj *  buildAdder(
                    PDTNumAbcObj & inps1, //!< Input 1 bit vector
                    PDTNumAbcObj & inps2, //!< Input 2 bit vector
                    PDTBoolAbcObj & ovflow //!< overflow bit to return
                    );

        /**
         * @brief Build a one bit and gate
         * @return PDTBoolAbcObj * 
         */
        PDTBoolAbcObj *
        buildOneBitAndGate(PDTBoolAbcObj & in1, //!< The first input bit
            PDTBoolAbcObj & in2 //!< The second input bit
            );

        /**
         * @brief Build a one bit or gate
         * @return PDTBoolAbcObj * 
         */
        PDTBoolAbcObj *
        buildOneBitOrGate(PDTBoolAbcObj & in1, //!< The first input bit
            PDTBoolAbcObj & in2 //!< The second input bit
            );

        /**
         * @brief Build the constant 0 bit
         * @returns An abc object representing the 0 constant
         * Originally written by Mario Achkar
         */
        PDTBoolAbcObj * get0();

        /**
         * @brief Build the constant 1 bit
         * @returns An abc object representing the 1 constant
         * Originally written by Mario Achkar
         */
        PDTBoolAbcObj * get1(); 

        /**
         * @brief Create a representation of a constant in abc
         * @return PDTNumAbcObj * 
         */
        PDTNumAbcObj * 
        convertConstant(int myconst, //!< The constant value to conver
                unsigned int aBound //!< register size
                );

        /**
         * @brief start the traversal
         */
        void start();

        /**
         * @brief get Abc object fanins
         * @return PDTNumAbcObj * containing all fanins
         */
        PDTNumAbcObj * 
        getFanins(PDTNumAbcObj * inpt //!< The input object
                );

        /**
         * @brief Set inpt1 as fanin to inpt1
         * @return returns true if success and false otherwise
         */
        bool 
        setFanins(PDTNumAbcObj * inpt1, //!< the objects to have fanins
                PDTNumAbcObj * fanins //!< the fanins
                );

        /**
         * @brief get bool abc objects fanin
         * @return returns the fanin of the current input
         */
        PDTBoolAbcObj *
        getBoolFanins(PDTBoolAbcObj * inpt //!< The input bit
                );

        /**
         * @brief Set fanin for a boolean object
         * @return true if succes
         */
        bool
        setBoolFanins(PDTBoolAbcObj * inpt1, //!< The bool to have fanin
                PDTBoolAbcObj * fanin //!< The fanin
                );
        /**
         * @brief Add primary input to boolean var
         */
        void
        addPi(PDTBoolAbcObj & boolObj, //!< The bool obj to add to  
                const char * name //!< The name to assign
                );

        /** 
         * @brief Add primary output to boolean var
         */
        void
        addPo(PDTBoolAbcObj & boolObj, //!< The bool obj to add to 
                const char * name //!< The name to assign
                );

        /**
         * @brief perform less then operation
         * @return returns a < b
         */
        PDTBoolAbcObj *
        lt(PDTNumAbcObj * a, //!< The first input
            PDTNumAbcObj * b //!< The second input
            );

        Abc_Obj_t * 
        lt(PDTNumAbcObj * a,
            PDTNumAbcObj *b, 
            unsigned int i
            );

        /**
         * @brief perform greater than operation
         * @return returns a > b
         */
        PDTBoolAbcObj * 
        gt(PDTNumAbcObj * a, //!< The first input
           PDTNumAbcObj * b //!< The second input
           );

        /**
         * @brief compares two input num objects
         * @return ret = (a == b)
         */
        PDTBoolAbcObj * 
        eq(PDTNumAbcObj * a, //!< The first input
            PDTNumAbcObj * b //!< The second input
            );

        // utility functions //
        void buildControl();

        void checkStructure();
        void Command(const char * cmd);
        void interActiveCmd();

        inline void updaterVisitNode(PDTNode * node);
        void checkParents(PDTNode * node);
        void fixAssign(PDTNode * node);
        void fixIfElse(PDTNode * node);
        void fixWhile(PDTNode * node);
        bool isLHS(PDTSequenceAccessNum & d);

        void 
        transposeVectors(vector < PDTNumAbcObj * > & ret, 
            PDTNumAbcObj ** inps, unsigned int size);
        void
        transposeVectors(vector<PDTNumAbcObj*> & ret, 
            vector<PDTNumAbcObj*> & inps, unsigned int size);
        void setUpPcVector(vector < PDTNumAbcObj * > & in);
        void createPOs(PDTNumAbcObj * in, const char * name);
        void createPO(PDTBoolAbcObj * in, const char * name);
        void createPIs(PDTNumAbcObj * in, const char * name);
        PDTBoolAbcObj * buildNot(PDTBoolAbcObj * in);
        void PDTProve();
};


#endif
